es_realizer{i:l} r es_realizer{i':l} 

latex

Definitions	suptype(S; T), S  T, x. t(x), x:A. B(x), DeclaredType(ds;x), t  T, P  Q, x(s), Unit, Realizer, Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rpre(loc;ds;a;p;P), Rsends(ds;knd;T;l;dt;g), Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), left  right, Rnone(),
Lemmas	Rrframe wf, Rbframe wf, Raframe wf, Rpre wf, Rsends wf, id-deq wf, fpf-cap wf, strong-subtype-self, subtype-fpf3, Reffect wf, Rsframe wf, Rframe wf, Rinit wf, Rplus wf, Rnone wf, bool wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, rationals wf, Id wf, unit wf, es realizer wf